A general goal of computer program verification is to discover invariants that are strong enough to verify given assertions in a program in order to prove program correctness and/or find bugs. Traditionally, iterative fixed-point computation based techniques like data-flow analyses, abstract interpretation or model checking have been used for discovering these invariants.
An alternative is to use a constraint-based invariant generation technique. Constraint-based techniques offer advantages over fixed-point computation based techniques, including that they are goal-directed and thus have the potential to be more efficient. Another advantage is that they do not require the use of widening heuristics that are used by fixed-point based techniques which lead to loss of precision that is often hard to control. However, current constraint-based techniques are limited in a number of ways.